\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $l$:($\mathbb{N}$ List), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List), $n$:$\mathbb{N}$.
\-\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; ecl{-}add{-}catch($v$; $l$))($n$,$L$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=((($\neg$($n$ $\in$ $l$)) $\wedge$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($n$,$L$)))\+
\\[0ex]$\vee$ (($n$ = 0 $\in$ $\mathbb{Z}$) $\wedge$ l\_exists($l$; $\mathbb{N}$; $m$.(ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $v$)($m$,$L$)))))
\-
\end{tabbing}